\begin{tabbing}
abs{-}fifo\{i:l\}($C$; $T$)(${\it es}$,${\it In}$,${\it Out}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:$C$.\+
\\[0ex]$\exists$\=$f$:\{$e$:es{-}E(${\it es}$)$\mid$ abs{-}R($C$;${\it Out}$)($i$,$e$)\} $\rightarrow$\{$e$:es{-}E(${\it es}$)$\mid$ $\exists$$j$:$C$. (abs{-}S($C$;${\it In}$)($j$,$i$,$e$))\} \+
\\[0ex](antecedent{-}surjection(${\it es}$;$\lambda$$e$.abs{-}R($C$;${\it Out}$)($i$,$e$);$\lambda$$e$.$\exists$$j$:$C$. (abs{-}S($C$;${\it In}$)($j$,$i$,$e$));$f$)
\\[0ex]\& (\=$\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ abs{-}R($C$;${\it Out}$)($i$,$e$)\} , $j$:\{$j$:$C$$\mid$ abs{-}S($C$;${\it In}$)($j$,$i$,$f$($e$))\} .\+
\\[0ex](${\it Out}$($e$).2) = (${\it In}$($f$($e$)).2) $\in$ $T$)
\-\\[0ex]\& (\=$\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ abs{-}R($C$;${\it Out}$)($i$,$e$)\} , ${\it e'}$:\{$e$:es{-}E(${\it es}$)$\mid$ abs{-}R($C$;${\it Out}$)($i$,$e$)\} , $j$:$C$.\+
\\[0ex](abs{-}S($C$;${\it In}$)($j$,$i$,$f$($e$)))
\\[0ex]$\Rightarrow$ (abs{-}S($C$;${\it In}$)($j$,$i$,$f$(${\it e'}$)))
\\[0ex]$\Rightarrow$ es{-}causle(${\it es}$;$f$($e$);$f$(${\it e'}$))
\\[0ex]$\Rightarrow$ es{-}causle(${\it es}$;$e$;${\it e'}$)))
\-\-\-
\end{tabbing}